retrace(es; Q; X)
== (e, e':E. (Q(e,e'))  (((e  X)) & ((e'  X))))
== & (e, e':E(X). (Q(e,e'))  (e = e')  (Q(e',e)))
== & (e':E.
== & (L:E List
== & (((e:E. (e  L)  (Q(e,e'))) & (e1, e2:E. e1 before e2  L  (Q(e1,e2))))) 

latex

---

clarification:

retrace(es; Q; X)
== (e:es-E(es), e':es-E(es). (Q(e,e'))  (((e  X)) & ((e'  X))))
== & (e:es-E-interface(es;X), e':es-E-interface(es;X). (Q(e,e'))  (e = e'  es-E(es))  (Q(e',e)))
== & (e':es-E(es).
== & (L:es-E(es) List
== & (((e:es-E(es). (e  L  es-E(es))  (Q(e,e')))
== & (& (e1:es-E(es), e2:es-E(es). e1 before e2  L  es-E(es)  (Q(e1,e2))))) 

latex

Definitions	b, e  X, E(X), P  Q, s = t, x:A. B(x), type List, P & Q, P  Q, (x  l), x:A. B(x), P  Q, x before y  l, E, f(a)
FDL editor aliases	retrace